COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		outline
C00005 00003	There  is a  large  area of  contemporary  mathematics which  can  be
C00007 00004	Rather than simply publish another paper on the applications of
C00008 ENDMK
C⊗;
	outline

description of existing system
 input/output format
 on-line features
 compare with others
  Bledsoe  -for natural i/o
  Guard    -for on-line
  Wos & ?  -for strategy lang.
  Nevins   -for ?
 don't say much about insides- not relevant.

examples
 marsden: verif
 geometry:explor
 tba:     verif 
 cowan:   verif and explor
 houses:  prog.lang.  (c.f. jfs disjunctions)

general discussion of existing system
 what's good
  natural i/0
   better than B&B
  partitioning, but should be broadened
 what's bad
  subproblem control--general control problem
   getting instantiations back
  must be able to express intuitions in terms of control

applications
 simple mathematics -desk calculator
 intuition builder  -for beginner

conclusions
 tp. like this one are limited
  is resolution the way?
 completeness downplayed
  work this back into discussion of examples
 incompleteness manifestation:
   in the strategies
   in the use of on-line
 ever used completeness in positive way? i.e. "no-proof found" => ... .
 key issue: logic validity of rules 
            computationally sound (don't take forever?)

extensions
 how about typing and a.d.s.?
 languages for tp.
  description of primitives -substitution, application
  control structures  -reasonably wild control: suspend, resume, kill, ...
  data structures
  attempt to discover by looking at examples (ours and Bledsoe and Bruell)
    also look at prove1.new in abstract form.
  how about induction: goal structure?
There  is a  large  area of  contemporary  mathematics which  can  be
profitably explored  using an interactive first-order theorem prover.
This report will  describe #  applications of the  the Stanford  A.I.
Project's theorem prover. 

The first application explores the  field of Euclidean Geometry.  The
second   example   deals  with   abstract  algebra,   in  particular,
Implicative models.  Third, we used some of the programmable features
of the prover to give a solution to a puzzle. 

justification for paper at this late date.   implications
rather than results.

usefulness of t.ps's ;  an appreciation of their place in the scheme
of computational tools.

past over-sold; in face of intuition and common sense

Rather than simply publish another paper on the applications of
first-order theorem prover applications, we feel that it is
important to try to take stock of the past perforamnce
and future expectations of this field.

We will present a few diverse results from our history of theorem proving
but present them not as bench-marks which to challenge other
provers. These examples were selected to highlight defects in
the current schemes or to  exemplify certain technques whichwe
feel hold promise for future applications.